/-
Copyright (c) 2021 Riccardo Brasca. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Riccardo Brasca
-/
import Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.FieldTheory.Galois.Basic

/-!
# Cyclotomic extensions

Let `A` and `B` be commutative rings with `Algebra A B`. For `S : Set ℕ`, we define a class
`IsCyclotomicExtension S A B` expressing the fact that `B` is obtained from `A` by adding `n`-th
primitive roots of unity, for all nonzero `n ∈ S`.

## Main definitions

* `IsCyclotomicExtension S A B` : means that `B` is obtained from `A` by adding `n`-th primitive
  roots of unity, for all nonzero `n ∈ S`.
* `CyclotomicField`: given `n : ℕ` and a field `K`, we define `CyclotomicField n K` as the
  splitting field of `cyclotomic n K`. If `n` is nonzero in `K`, it has the instance
  `IsCyclotomicExtension {n} K (CyclotomicField n K)`.
* `CyclotomicRing` : if `A` is a domain with fraction field `K` and `n : ℕ`, we define
  `CyclotomicRing n A K` as the `A`-subalgebra of `CyclotomicField n K` generated by the roots of
  `X ^ n - 1`. If `n` is nonzero in `A`, it has the instance
  `IsCyclotomicExtension {n} A (CyclotomicRing n A K)`.

## Main results

* `IsCyclotomicExtension.trans` : if `IsCyclotomicExtension S A B` and
  `IsCyclotomicExtension T B C`, then `IsCyclotomicExtension (S ∪ T) A C` if
  `Function.Injective (algebraMap B C)`.
* `IsCyclotomicExtension.union_right` : given `IsCyclotomicExtension (S ∪ T) A B`, then
  `IsCyclotomicExtension T (adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ (a : ℕ) = 1 }) B`.
* `IsCyclotomicExtension.union_left` : given `IsCyclotomicExtension T A B` and `S ⊆ T`, then
  `IsCyclotomicExtension S A (adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ (a : ℕ) = 1 })`.
* `IsCyclotomicExtension.finite` : if `S` is finite and `IsCyclotomicExtension S A B`, then
  `B` is a finite `A`-algebra.
* `IsCyclotomicExtension.numberField` : a finite cyclotomic extension of a number field is a
  number field.
* `IsCyclotomicExtension.isSplittingField_X_pow_sub_one` : if `IsCyclotomicExtension {n} K L`,
  then `L` is the splitting field of `X ^ n - 1`.
* `IsCyclotomicExtension.splitting_field_cyclotomic` : if `IsCyclotomicExtension {n} K L`,
  then `L` is the splitting field of `cyclotomic n K`.

## Implementation details

Our definition of `IsCyclotomicExtension` is very general, to allow rings of any characteristic
and infinite extensions, but it will mainly be used in the case `S = {n}` and for integral domains.
All results are in the `IsCyclotomicExtension` namespace.
Note that some results, for example `IsCyclotomicExtension.trans`,
`IsCyclotomicExtension.finite`, `IsCyclotomicExtension.numberField`,
`IsCyclotomicExtension.finiteDimensional`, `IsCyclotomicExtension.isGalois` and
`CyclotomicField.algebraBase` are lemmas, but they can be made local instances. Some of them are
included in the `Cyclotomic` locale.

-/


open Polynomial Algebra Module Set

universe u v w z

noncomputable section

/-- Given an `A`-algebra `B` and `S : Set ℕ`, we define `IsCyclotomicExtension S A B` requiring
that there is an `n`-th primitive root of unity in `B` for all nonzero `n ∈ S` and that
`B` is generated over `A` by the roots of `X ^ n - 1`. -/
@[mk_iff]
class IsCyclotomicExtension
    (S : Set ℕ) (A : Type u) (B : Type v)
    [CommRing A] [CommRing B] [Algebra A B] : Prop where
  /-- For all nonzero `n ∈ S`, there exists a primitive `n`-th root of unity in `B`. -/
  exists_isPrimitiveRoot {S} (A B) {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0) :
    ∃ r : B, IsPrimitiveRoot r n
  /-- The `n`-th roots of unity, for `n ∈ S` nonzero, generate `B` as an `A`-algebra. -/
  adjoin_roots : ∀ x : B, x ∈ adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}

variable (n : ℕ) [NeZero n] (S T : Set ℕ) (A : Type u) (B : Type v) (K : Type w) (L : Type z)
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]

namespace IsCyclotomicExtension

section Basic

variable {S B} in
@[deprecated exists_isPrimitiveRoot (since := "2025-05-21")]
theorem exists_prim_root [IsCyclotomicExtension S A B] {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0) :
    ∃ r : B, IsPrimitiveRoot r n :=
  exists_isPrimitiveRoot A B ha ha'

/-- A reformulation of `IsCyclotomicExtension` that uses `⊤`. -/
theorem iff_adjoin_eq_top :
    IsCyclotomicExtension S A B ↔
      (∀ n : ℕ, n ∈ S → n ≠ 0 → ∃ r : B, IsPrimitiveRoot r n) ∧
        adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1} = ⊤ :=
  ⟨fun h => ⟨fun _ => h.exists_isPrimitiveRoot, Algebra.eq_top_iff.2 h.adjoin_roots⟩, fun h =>
    ⟨h.1 _, Algebra.eq_top_iff.1 h.2⟩⟩

/-- A reformulation of `IsCyclotomicExtension` in the case `S` is a singleton. -/
theorem iff_singleton :
    IsCyclotomicExtension {n} A B ↔
      (∃ r : B, IsPrimitiveRoot r n) ∧ ∀ x, x ∈ adjoin A {b : B | b ^ n = 1} := by
  simp [isCyclotomicExtension_iff, NeZero.ne]

/-- If `IsCyclotomicExtension ∅ A B`, then the image of `A` in `B` equals `B`. -/
theorem empty [h : IsCyclotomicExtension ∅ A B] : (⊥ : Subalgebra A B) = ⊤ := by
  simpa [Algebra.eq_top_iff, isCyclotomicExtension_iff] using h

theorem eq_self_sdiff_zero :
    IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B := by
  simp [isCyclotomicExtension_iff, and_assoc]

/-- If `IsCyclotomicExtension {1} A B`, then the image of `A` in `B` equals `B`. -/
theorem singleton_one [h : IsCyclotomicExtension {1} A B] : (⊥ : Subalgebra A B) = ⊤ :=
  Algebra.eq_top_iff.2 fun x => by
    simpa [adjoin_singleton_one] using ((isCyclotomicExtension_iff _ _ _).1 h).2 x

variable {A B}

/-- If `(⊥ : SubAlgebra A B) = ⊤`, then `IsCyclotomicExtension ∅ A B`. -/
theorem singleton_zero_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) :
    IsCyclotomicExtension ∅ A B := by
  refine (iff_adjoin_eq_top _ _ _).2
    ⟨fun s hs => by simp at hs, _root_.eq_top_iff.2 fun x hx => ?_⟩
  rw [← h] at hx
  simpa using hx

variable (A B)

/-- Transitivity of cyclotomic extensions. -/
theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
    [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C]
    (h : Function.Injective (algebraMap B C)) : IsCyclotomicExtension (S ∪ T) A C := by
  refine ⟨fun hn => ?_, fun x => ?_⟩
  · intro hn'
    rcases hn with hn | hn
    · obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'
      refine ⟨algebraMap B C b, ?_⟩
      exact hb.map_of_injective h
    · exact ((isCyclotomicExtension_iff _ _ _).1 hT).1 hn hn'
  · refine adjoin_induction (hx := ((isCyclotomicExtension_iff T B _).1 hT).2 x)
      (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => ?_)
      (fun x y _ _ hx hy => Subalgebra.add_mem _ hx hy)
      fun x y _ _ hx hy => Subalgebra.mul_mem _ hx hy
    let f := IsScalarTower.toAlgHom A B C
    have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}).map f :=
      ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩
    rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb
    refine adjoin_mono (fun y hy => ?_) hb
    obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy
    exact ⟨n, ⟨mem_union_left T hn.1, hn.2.1, by rw [← h₁, ← map_pow, hn.2.2, map_one]⟩⟩

@[nontriviality]
theorem subsingleton_iff [Subsingleton B] :
    IsCyclotomicExtension S A B ↔ S ⊆ {0, 1} := by
  have : Subsingleton (Subalgebra A B) := inferInstance
  refine ⟨fun ⟨hprim, _⟩ ↦ ?_, fun hS ↦ ?_⟩
  · refine subset_pair_iff.mpr fun s hs ↦ or_iff_not_imp_left.mpr fun hs' ↦ ?_
    obtain ⟨ζ, hζ⟩ := hprim hs hs'
    exact mod_cast hζ.unique (IsPrimitiveRoot.of_subsingleton ζ)
  · refine ⟨fun {s} hs hs' ↦ ?_, fun x ↦ by convert (mem_top (R := A) : x ∈ ⊤)⟩
    · have : s = 1 := (subset_pair_iff.mp hS s hs).resolve_left hs'
      exact ⟨0, this ▸ IsPrimitiveRoot.of_subsingleton 0⟩

/-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B`
is a cyclotomic extension of `adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 }` given by
roots of unity of order in `T`. -/
theorem union_right [h : IsCyclotomicExtension (S ∪ T) A B] :
    IsCyclotomicExtension T (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}) B := by
  have : {b : B | ∃ n : ℕ, n ∈ S ∪ T ∧ n ≠ 0 ∧ b ^ n = 1} =
      {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1} ∪
        {b : B | ∃ n : ℕ, n ∈ T ∧ n ≠ 0 ∧ b ^ n = 1} := by
    refine le_antisymm ?_ ?_
    · rintro x ⟨n, hn₁ | hn₂, hnpow⟩
      · left; exact ⟨n, hn₁, hnpow⟩
      · right; exact ⟨n, hn₂, hnpow⟩
    · rintro x (⟨n, hn⟩ | ⟨n, hn⟩)
      · exact ⟨n, Or.inl hn.1, hn.2⟩
      · exact ⟨n, Or.inr hn.1, hn.2⟩
  refine ⟨fun hn => ((isCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => ?_⟩
  replace h := ((isCyclotomicExtension_iff _ _ _).1 h).2 b
  rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h

/-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `T` and `S ⊆ T`,
then `adjoin A { b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1 }` is a cyclotomic extension of `B`
given by roots of unity of order in `S`. -/
theorem union_left [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) :
    IsCyclotomicExtension S A (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}) := by
  refine ⟨@fun n hn hn' => ?_, fun b => ?_⟩
  · obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) hn'
    refine ⟨⟨b, subset_adjoin ⟨n, hn, hn', hb.pow_eq_one⟩⟩, ?_⟩
    rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
  · convert mem_top (R := A) (x := b)
    rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq]
    norm_cast

variable {n S}

/-- If there exists a nonzero `s ∈ S` such that `n ∣ s`, then `IsCyclotomicExtension S A B`
implies `IsCyclotomicExtension (S ∪ {n}) A B`. -/
theorem of_union_of_dvd (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) [H : IsCyclotomicExtension S A B] :
    IsCyclotomicExtension (S ∪ {n}) A B := by
  refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩
  · rw [mem_union, mem_singleton_iff] at hs
    obtain hs | rfl := hs
    · exact H.exists_isPrimitiveRoot hs hs'
    · obtain ⟨m, hm, hm', ⟨x, rfl⟩⟩ := h
      obtain ⟨ζ, hζ⟩ := H.exists_isPrimitiveRoot hm hm'
      refine ⟨ζ ^ x, ?_⟩
      have h_xnz : x ≠ 0 := Nat.ne_zero_of_mul_ne_zero_right hm'
      have := hζ.pow_of_dvd h_xnz (dvd_mul_left x s)
      rwa [mul_div_cancel_right₀ _ h_xnz] at this
  · refine _root_.eq_top_iff.2 ?_
    rw [← ((iff_adjoin_eq_top S A B).1 H).2]
    refine adjoin_mono fun x hx ↦ ?_
    simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢
    obtain ⟨m, hm, hm'⟩ := hx
    exact ⟨m, ⟨Or.inr hm, hm'⟩⟩

/-- If there exists a nonzero `s ∈ S` such that `n ∣ s`, then `IsCyclotomicExtension S A B`
  if and only if `IsCyclotomicExtension (S ∪ {n}) A B`. -/
theorem iff_union_of_dvd (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) :
    IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B := by
  refine
    ⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2
      ⟨fun s hs ↦ ?_, ?_⟩⟩
  · exact H.exists_isPrimitiveRoot (subset_union_left hs)
  · rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ A B).1 H).2]
    refine adjoin_mono fun x hx => ?_
    simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢
    obtain ⟨m, rfl | hm, hxpow⟩ := hx
    · obtain ⟨y, ⟨hy, hy', ⟨z, rfl⟩⟩⟩ := h
      exact ⟨_, ⟨hy, hy', by simp only [pow_mul, hxpow, one_pow]⟩⟩
    · exact ⟨m, ⟨hm, hxpow⟩⟩

variable (n S)

/-- `IsCyclotomicExtension S A B` is equivalent to `IsCyclotomicExtension (S ∪ {1}) A B`. -/
theorem iff_union_singleton_one :
    IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B := by
  by_cases hS: ∃ s ∈ S, s ≠ 0
  · exact iff_union_of_dvd _ _ (by simpa)
  · rw [eq_self_sdiff_zero S, eq_self_sdiff_zero (S ∪ {1}), union_diff_distrib,
      show S \ {0} = ∅ by aesop, empty_union, show {1} \ {0} = {1} by aesop]
    refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
    · refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs _ ↦ ⟨1, by simp [mem_singleton_iff.1 hs]⟩, ?_⟩
      simp [adjoin_singleton_one, empty]
    · refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩
      simp [singleton_one]

variable {A B}

/-- If `(⊥ : SubAlgebra A B) = ⊤`, then `IsCyclotomicExtension {1} A B`. -/
theorem singleton_one_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) :
    IsCyclotomicExtension {1} A B := by
  convert (iff_union_singleton_one _ A _).1 (singleton_zero_of_bot_eq_top h)
  simp

/-- If `Function.Surjective (algebraMap A B)`, then `IsCyclotomicExtension {1} A B`. -/
theorem singleton_one_of_algebraMap_bijective (h : Function.Surjective (algebraMap A B)) :
    IsCyclotomicExtension {1} A B :=
  singleton_one_of_bot_eq_top (surjective_algebraMap_iff.1 h).symm

variable (A B)

/-- Given `(f : B ≃ₐ[A] C)`, if `IsCyclotomicExtension S A B` then
`IsCyclotomicExtension S A C`. -/
protected
theorem equiv {C : Type*} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension S A B]
    (f : B ≃ₐ[A] C) : IsCyclotomicExtension S A C := by
  letI : Algebra B C := f.toAlgHom.toRingHom.toAlgebra
  haveI : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective
  haveI : IsScalarTower A B C := IsScalarTower.of_algHom f.toAlgHom
  exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)

protected
theorem neZero [h : IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero (n : B) := by
  obtain ⟨⟨r, hr⟩, -⟩ := (iff_singleton n A B).1 h
  exact hr.neZero'

protected
theorem neZero' [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero (n : A) := by
  have := IsCyclotomicExtension.neZero n A B
  exact NeZero.nat_of_neZero (algebraMap A B)

end Basic

section Fintype

theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension {n} A B] :
    Module.Finite A B := by
  classical
  rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
  refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
  · simp only [mem_singleton_iff, exists_eq_left]
    have : {b : B | n ≠ 0 ∧ b ^ n = 1} = (nthRoots n (1 : B)).toFinset :=
      Set.ext fun x ↦ ⟨fun h ↦ by simpa [n.pos_of_neZero] using h.2,
        fun h ↦ by simpa [n.pos_of_neZero, NeZero.ne n] using h⟩
    rw [this]
    exact (nthRoots n 1).toFinset.finite_toSet
  · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hb
    exact ⟨X ^ n - 1,
      ⟨monic_X_pow_sub_C _ (hb.1 ▸ NeZero.ne _), by simpa [sub_eq_zero] using hb.2.2⟩⟩

/-- If `S` is finite and `IsCyclotomicExtension S A B`, then `B` is a finite `A`-algebra. -/
protected theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] :
    Module.Finite A B := by
  rw [finite_coe_iff] at h₁
  induction S, h₁ using Set.Finite.induction_on generalizing h₂ A B with
  | empty =>
    refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
    simp [← top_toSubmodule, ← empty, toSubmodule_bot, Submodule.one_eq_span]
  | @insert n S _ _ H =>
    by_cases hn : n = 0
    · have : insert n S \ {0} = S \ {0} := by aesop
      rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂
      exact H A B
    have : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) :=
        union_left _ (insert n S) _ _ (subset_insert n S)
    have := H A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1})
    have : Module.Finite (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) B := by
      rw [← union_singleton] at h₂
      let _ := union_right S {n} A B
      have : NeZero n := ⟨hn⟩
      exact finite_of_singleton n _ _
    exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _

/-- A cyclotomic finite extension of a number field is a number field. -/
theorem numberField [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] : NumberField L :=
  { to_charZero := charZero_of_injective_algebraMap (algebraMap K L).injective
    to_finiteDimensional := by
      haveI := charZero_of_injective_algebraMap (algebraMap K L).injective
      haveI := IsCyclotomicExtension.finite S K L
      exact Module.Finite.trans K _ }

/-- A finite cyclotomic extension of an integral noetherian domain is integral -/
theorem integral [IsDomain B] [IsNoetherianRing A] [Finite S] [IsCyclotomicExtension S A B] :
    Algebra.IsIntegral A B :=
  have := IsCyclotomicExtension.finite S A B
  ⟨isIntegral_of_noetherian inferInstance⟩

/-- If `S` is finite and `IsCyclotomicExtension S K A`, then `finiteDimensional K A`. -/
theorem finiteDimensional (C : Type z) [Finite S] [CommRing C] [Algebra K C] [IsDomain C]
    [IsCyclotomicExtension S K C] : FiniteDimensional K C :=
  IsCyclotomicExtension.finite S K C

end Fintype

section

variable {A B}

theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : ℕ} [NeZero n]
    (hζ : IsPrimitiveRoot ζ n) :
    adjoin A ((cyclotomic n A).rootSet B) =
      adjoin A {b : B | ∃ a : ℕ, a ∈ ({n} : Set ℕ) ∧ a ≠ 0 ∧ b ^ a = 1} := by
  simp only [mem_singleton_iff, exists_eq_left, map_cyclotomic]
  refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)
  · rw [mem_rootSet'] at hx
    simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq]
    rw [isRoot_of_unity_iff (NeZero.pos n)]
    refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
    rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def]
    exact hx.2
  · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx
    obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2
    refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)
    rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot]
    exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos n)⟩

theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ} [NeZero n] [IsDomain B] {ζ : B}
    (hζ : IsPrimitiveRoot ζ n) : adjoin A ((cyclotomic n A).rootSet B) = adjoin A {ζ} := by
  refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)
  · suffices hx : x ^ n = 1 by
      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
      exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
    refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_
    refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
    rw [mem_rootSet', aeval_def, ← eval_map, map_cyclotomic, ← IsRoot] at hx
    exact hx.2
  · simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx
    simpa only [hx, mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, IsRoot] using
      And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic (NeZero.pos n))

theorem adjoin_primitive_root_eq_top {n : ℕ} [NeZero n] [IsDomain B]
    [h : IsCyclotomicExtension {n} A B]
    {ζ : B} (hζ : IsPrimitiveRoot ζ n) : adjoin A ({ζ} : Set B) = ⊤ := by
  classical
  rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
  rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
  exact ((iff_adjoin_eq_top {n} A B).mp h).2

variable (A)

theorem _root_.IsPrimitiveRoot.adjoin_isCyclotomicExtension {ζ : B} {n : ℕ} [NeZero n]
    (h : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} A (adjoin A ({ζ} : Set B)) :=
  { exists_isPrimitiveRoot := fun hi hi' => by
      rw [Set.mem_singleton_iff] at hi
      refine ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩
      rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]
    adjoin_roots := fun ⟨x, hx⟩ => by
      refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
      · rw [Set.mem_singleton_iff] at hb
        refine subset_adjoin ?_
        simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq, hb]
        rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
        exact ⟨NeZero.ne n, ((IsPrimitiveRoot.iff_def ζ n).1 h).1⟩
      · exact Subalgebra.algebraMap_mem _ _
      · exact Subalgebra.add_mem _ hb₁ hb₂
      · exact Subalgebra.mul_mem _ hb₁ hb₂ }

end

section Field

variable {n S}

/-- A cyclotomic extension splits `X ^ n - 1` if `n ∈ S`. -/
theorem splits_X_pow_sub_one [H : IsCyclotomicExtension S K L] (hS : n ∈ S) :
    Splits (algebraMap K L) (X ^ n - 1) := by
  rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X]
  obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)
  exact X_pow_sub_one_splits hz

/-- A cyclotomic extension splits `cyclotomic n K` if `n ∈ S`. -/
theorem splits_cyclotomic [IsCyclotomicExtension S K L] (hS : n ∈ S) :
    Splits (algebraMap K L) (cyclotomic n K) := by
  refine splits_of_splits_of_dvd _ (X_pow_sub_C_ne_zero (NeZero.pos _) _)
    (splits_X_pow_sub_one K L hS) ?_
  use ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i K
  rw [(eq_cyclotomic_iff (NeZero.pos _) _).1 rfl, RingHom.map_one]

variable (n S)

section Singleton

variable [IsCyclotomicExtension {n} K L]

/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `X ^ n - 1`. -/
theorem isSplittingField_X_pow_sub_one : IsSplittingField K L (X ^ n - 1) :=
  { splits' := splits_X_pow_sub_one K L (mem_singleton n)
    adjoin_rootSet' := by
      rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]
      congr
      refine Set.ext fun x => ?_
      simp only [mem_singleton_iff, ne_eq, exists_eq_left, NeZero.ne, not_false_eq_true, true_and,
        mem_setOf_eq]
      simp only [mem_rootSet', map_sub, map_pow, aeval_one, aeval_X, sub_eq_zero, map_X,
        and_iff_right_iff_imp, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one]
      exact fun _ => X_pow_sub_C_ne_zero (NeZero.pos n) (1 : L) }

/-- Any two `n`-th cyclotomic extensions are isomorphic. -/
def algEquiv (L' : Type*) [Field L'] [Algebra K L'] [IsCyclotomicExtension {n} K L'] :
    L ≃ₐ[K] L' :=
  let h₁ := isSplittingField_X_pow_sub_one n K L
  let h₂ := isSplittingField_X_pow_sub_one n K L'
  (@IsSplittingField.algEquiv K L _ _ _ (X ^ n - 1) h₁).trans
    (@IsSplittingField.algEquiv K L' _ _ _ (X ^ n - 1) h₂).symm

scoped[Cyclotomic] attribute [instance] IsCyclotomicExtension.isSplittingField_X_pow_sub_one

include n in
theorem isGalois : IsGalois K L :=
  letI := isSplittingField_X_pow_sub_one n K L
  IsGalois.of_separable_splitting_field (X_pow_sub_one_separable_iff.2
    (IsCyclotomicExtension.neZero' n K L).1)

/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `cyclotomic n K`. -/
theorem splitting_field_cyclotomic : IsSplittingField K L (cyclotomic n K) :=
  { splits' := splits_cyclotomic K L (mem_singleton n)
    adjoin_rootSet' := by
      rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]
      letI := Classical.decEq L
      -- todo: make `exists_prim_root` take an explicit `L`
      obtain ⟨ζ : L, hζ⟩ :=
        IsCyclotomicExtension.exists_isPrimitiveRoot K (B := L) (mem_singleton n) (NeZero.ne _)
      exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ }

scoped[Cyclotomic] attribute [instance] IsCyclotomicExtension.splitting_field_cyclotomic

end Singleton

end Field

end IsCyclotomicExtension

section CyclotomicField

/-- Given a nonzero `n : ℕ` and a field `K`, we define `CyclotomicField n K` as the
splitting field of `cyclotomic n K`. If `n` is nonzero in `K`, it has
the instance `IsCyclotomicExtension {n} K (CyclotomicField n K)`. -/
def CyclotomicField : Type w :=
  (cyclotomic n K).SplittingField

namespace CyclotomicField

instance : Field (CyclotomicField n K) := by
  delta CyclotomicField; infer_instance

instance algebra : Algebra K (CyclotomicField n K) := by
  delta CyclotomicField; infer_instance

instance : Inhabited (CyclotomicField n K) := by
  delta CyclotomicField; infer_instance

instance [CharZero K] : CharZero (CyclotomicField n K) :=
  charZero_of_injective_algebraMap (algebraMap K _).injective

instance isCyclotomicExtension [NeZero (n : K)] :
    IsCyclotomicExtension {n} K (CyclotomicField n K) := by
  have : NeZero (n : CyclotomicField n K) :=
    NeZero.nat_of_injective (algebraMap K _).injective
  letI := Classical.decEq (CyclotomicField n K)
  obtain ⟨ζ, hζ⟩ :=
    exists_root_of_splits (algebraMap K (CyclotomicField n K)) (SplittingField.splits _)
      (degree_cyclotomic_pos n K (NeZero.pos n)).ne'
  rw [← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ
  refine ⟨?_, ?_⟩
  · simp only [mem_singleton_iff, forall_eq]
    exact fun _ ↦ ⟨ζ, hζ⟩
  · rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm]
    exact IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

instance [NumberField K] : NumberField (CyclotomicField n K) :=
  IsCyclotomicExtension.numberField {n} K _

end CyclotomicField

end CyclotomicField

section IsDomain

variable [Algebra A K]

section CyclotomicRing

/-- If `K` is the fraction field of `A`, the `A`-algebra structure on `CyclotomicField n K`.
-/
@[nolint unusedArguments]
instance CyclotomicField.algebraBase : Algebra A (CyclotomicField n K) :=
  SplittingField.algebra' (cyclotomic n K)

/-- Ensure there are no diamonds when `A = ℤ` but there are `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906 -/
example : Ring.toIntAlgebra (CyclotomicField n ℚ) = CyclotomicField.algebraBase _ _ _ := rfl

instance CyclotomicField.algebra' {R : Type*} [CommRing R] [Algebra R K] :
    Algebra R (CyclotomicField n K) :=
  SplittingField.algebra' (cyclotomic n K)

instance {R : Type*} [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicField n K) :=
  SplittingField.isScalarTower _

instance [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicField n K) := by
  rw [NoZeroSMulDivisors.iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective,
    IsScalarTower.algebraMap_eq A K (CyclotomicField n K)]
  exact
    (Function.Injective.comp (FaithfulSMul.algebraMap_injective K (CyclotomicField n K))
      (IsFractionRing.injective A K) :)

/-- If `A` is a domain with fraction field `K` and `n : ℕ`, we define `CyclotomicRing n A K` as
the `A`-subalgebra of `CyclotomicField n K` generated by the roots of `X ^ n - 1`. If `n`
is nonzero in `A`, it has the instance `IsCyclotomicExtension {n} A (CyclotomicRing n A K)`. -/
@[nolint unusedArguments]
def CyclotomicRing : Type w :=
  adjoin A {b : CyclotomicField n K | b ^ n = 1}

namespace CyclotomicRing

instance : CommRing (CyclotomicRing n A K) := by
  delta CyclotomicRing; infer_instance

instance : IsDomain (CyclotomicRing n A K) := by
  delta CyclotomicRing; infer_instance

instance : Inhabited (CyclotomicRing n A K) := by
  delta CyclotomicRing; infer_instance

/-- The `A`-algebra structure on `CyclotomicRing n A K`. -/
instance algebraBase : Algebra A (CyclotomicRing n A K) :=
  (adjoin A _).algebra

-- Ensure that there is no diamonds with ℤ.
-- but there is at `reducible_and_instances` https://github.com/leanprover-community/mathlib4/issues/10906
example {n : ℕ} : CyclotomicRing.algebraBase n ℤ ℚ = Ring.toIntAlgebra _ := rfl

instance [IsFractionRing A K] :
    NoZeroSMulDivisors A (CyclotomicRing n A K) :=
  (adjoin A _).noZeroSMulDivisors_bot

omit [NeZero n] in
theorem algebraBase_injective [IsFractionRing A K] :
    Function.Injective <| algebraMap A (CyclotomicRing n A K) :=
  FaithfulSMul.algebraMap_injective _ _

instance : Algebra (CyclotomicRing n A K) (CyclotomicField n K) :=
  (adjoin A _).toAlgebra

omit [NeZero n] in
theorem adjoin_algebra_injective :
    Function.Injective <| algebraMap (CyclotomicRing n A K) (CyclotomicField n K) :=
  Subtype.val_injective

instance : NoZeroSMulDivisors (CyclotomicRing n A K) (CyclotomicField n K) :=
  NoZeroSMulDivisors.iff_algebraMap_injective.mpr (adjoin_algebra_injective n A K)

instance : IsScalarTower A (CyclotomicRing n A K) (CyclotomicField n K) :=
  IsScalarTower.subalgebra' _ _ _ _

instance isCyclotomicExtension [IsFractionRing A K] [NeZero ((n : ℕ) : A)] :
    IsCyclotomicExtension {n} A (CyclotomicRing n A K) where
  exists_isPrimitiveRoot := @fun a han => by
    rw [mem_singleton_iff] at han
    subst a
    have := NeZero.of_faithfulSMul A K n
    have := NeZero.of_faithfulSMul A (CyclotomicField n K) n
    obtain ⟨μ, hμ⟩ := (CyclotomicField.isCyclotomicExtension n K).exists_isPrimitiveRoot
      (mem_singleton n) (NeZero.ne n)
    refine fun _ ↦ ⟨⟨μ, subset_adjoin ?_⟩, ?_⟩
    · apply (isRoot_of_unity_iff (NeZero.pos n) (CyclotomicField n K)).mpr
      refine ⟨n, Nat.mem_divisors_self _ (NeZero.ne n), ?_⟩
      rwa [← isRoot_cyclotomic_iff] at hμ
    · rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
  adjoin_roots x := by
    obtain ⟨x, hx⟩ := x
    refine
      adjoin_induction (fun y hy => ?_) (fun a => ?_) (fun y z _ _ hy hz => ?_)
        (fun y z  _ _ hy hz => ?_) hx
    · refine subset_adjoin ?_
      simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq]
      exact ⟨NeZero.ne n, by rwa [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]⟩
    · exact Subalgebra.algebraMap_mem _ a
    · exact Subalgebra.add_mem _ hy hz
    · exact Subalgebra.mul_mem _ hy hz

instance [IsFractionRing A K] [IsDomain A] [NeZero (n : A)] :
    IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K) where
  map_units' := fun ⟨x, hx⟩ => by
    rw [isUnit_iff_ne_zero]
    apply map_ne_zero_of_mem_nonZeroDivisors
    · apply adjoin_algebra_injective
    · exact hx
  surj' x := by
    have : NeZero (n : K) := NeZero.nat_of_injective (IsFractionRing.injective A K)
    refine
      Algebra.adjoin_induction
        (hx := ((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1
            (CyclotomicField.isCyclotomicExtension n K)).2 x)
        (fun y hy => ?_) (fun k => ?_) ?_ ?_
    · exact ⟨⟨⟨y, subset_adjoin hy⟩, 1⟩, by simp; rfl⟩
    · have : IsLocalization (nonZeroDivisors A) K := inferInstance
      replace := this.surj
      obtain ⟨⟨z, w⟩, hw⟩ := this k
      refine ⟨⟨algebraMap A (CyclotomicRing n A K) z, algebraMap A (CyclotomicRing n A K) w,
        map_mem_nonZeroDivisors _ (algebraBase_injective n A K) w.2⟩, ?_⟩
      letI : IsScalarTower A K (CyclotomicField n K) :=
        IsScalarTower.of_algebraMap_eq (congr_fun rfl)
      rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
        @IsScalarTower.algebraMap_apply A K _ _ _ _ _ (_root_.CyclotomicField.algebra n K) _ _ w,
        ← RingHom.map_mul, hw, ← IsScalarTower.algebraMap_apply]
    · rintro y z - - ⟨a, ha⟩ ⟨b, hb⟩
      refine ⟨⟨a.1 * b.2 + b.1 * a.2, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
      rw [RingHom.map_mul, add_mul, ← mul_assoc, ha,
        mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, hb]
      simp only [map_add, map_mul]
    · rintro y z - - ⟨a, ha⟩ ⟨b, hb⟩
      refine ⟨⟨a.1 * b.1, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
      rw [RingHom.map_mul, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), mul_assoc, ←
        mul_assoc z, hb, ← mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, ha]
      simp only [map_mul]
  exists_of_eq {x y} h := ⟨1, by rw [adjoin_algebra_injective n A K h]⟩

theorem eq_adjoin_primitive_root {μ : CyclotomicField n K} (h : IsPrimitiveRoot μ n) :
    CyclotomicRing n A K = adjoin A ({μ} : Set (CyclotomicField n K)) := by
  rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
    IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]
  simp [CyclotomicRing, NeZero.ne n]

end CyclotomicRing

end CyclotomicRing

end IsDomain

section IsAlgClosed

variable [IsAlgClosed K]

/-- Algebraically closed fields are `S`-cyclotomic extensions over themselves if
`NeZero ((a : ℕ) : K))` for all nonzero `a ∈ S`. -/
theorem IsAlgClosed.isCyclotomicExtension (h : ∀ a ∈ S, a ≠ 0 → NeZero (a : K)) :
    IsCyclotomicExtension S K K := by
  rw [IsCyclotomicExtension.eq_self_sdiff_zero]
  refine ⟨@fun a ha ha' ↦ ?_, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩
  obtain ⟨r, hr⟩ := IsAlgClosed.exists_aeval_eq_zero K _
    (degree_cyclotomic_pos a K (Nat.pos_of_ne_zero ha')).ne'
  have : NeZero (a : K) := h a (mem_of_mem_diff ha) ha'
  exact ⟨r,  by rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr⟩

instance IsAlgClosedOfCharZero.isCyclotomicExtension [CharZero K] :
    ∀ S, IsCyclotomicExtension S K K := fun S => by
  rw [IsCyclotomicExtension.eq_self_sdiff_zero]
  exact IsAlgClosed.isCyclotomicExtension _ K fun _ _ h ↦ ⟨Nat.cast_ne_zero.mpr h⟩

end IsAlgClosed
